p:IdLnk List, i, j:Id. lconnects(p;i;j)  Prop 

latex

Definitions	null(as), False, P  Q, lconnects(p;i;j), lpath(p), P & Q, source(l), hd(l), Prop, destination(l), last(L), P  Q, x:A. B(x), A, b, ||as||, ij, Id, t  T, IdLnk
Lemmas	IdLnk wf, Id wf, non neg length, last wf, ldst wf, hd wf, lsrc wf, not wf, length wf1, lpath wf, assert of null, null wf, assert wf